(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i1 Int)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str2 String)
(declare-const Str3 String)
(declare-const Str4 String)
(declare-const Str5 String)
(declare-const Str10 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str14 String)
(declare-const Str18 String)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i10 Int)
(declare-const v12 Bool)
(declare-const v20 Bool)
(assert (>= (str.len Str18) 56))
(declare-const v21 Bool)
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v33 Bool)
(declare-const v34 Bool)
(declare-const i14 Int)
(declare-const v35 Bool)
(push)
(declare-const v37 Bool)
(push)
(push)
(push)
(assert (or v8 v21 (= "" Str4 "" "" (str.++ (str.++ (str.++ Str2 Str4) Str18) Str2 (int.to.str 663)))))
(assert (or (>= 0 208) v8 (distinct (str.++ "" "dfhxge" "") (str.++ (str.++ Str10 Str12) Str2) (str.++ (str.++ (str.++ Str2 Str4) Str18) Str12))))
(assert (or (str.contains "" "") (>= 0 208) (= "" Str4 "" "" "")))
(assert (or (= v3 v4 (< 0 0) (not (= v4 v3 v2 v9 (xor v6 v7 v8) (< 0 0) v0 (=> v1 v0) v6 (=> v1 v1) (=> v1 v0))) (not (= v4 v3 v2 v9 (xor v6 v7 v8) (< 0 0) v0 (=> v1 v0) v6 (=> v1 v1) (=> v1 v0))) v2) (>= 0 208) v8))
(assert (or (= (=> v1 v1) (not v1) (>= 729 0) (>= 208 0) (>= 0 208) (>= 0 0) v24 v34 v37) v8 (= (=> v1 v1) (not v1) (>= 729 0) (>= 208 0) (>= (* i10 (+ 208 78)) 208) (>= 0 0) v24 v34 v37)))
(assert (or (= "" Str4 "" "" "") (= 0 0) (= 0 0)))
(assert (or (=> v1 v0) (>= 0 208) v23))
(assert (or v3 (and v20 v8 v4 v5 v3 (=> v1 v1) (< 0 0) v2 v3) (str.suffixof Str2 "")))
(check-sat)
